COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	justification of flatten
C00005 ENDMK
C⊗;
;justification of flatten

(wipe-out)
(get-proofs lispax prf prf jk)

(proof flat)

(show high_order_definition)
;labels: HIGH_ORDER_DEFINITION 
(AXIOM
 |∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧
 			               DEFINED_FUN(X.Y)=
                                       BIGFUN(X,Y,DEFINED_FUN(X),DEFINED_FUN(Y))))|)

;now can define flatfun(x)=λy.flat(x,y)
;has to done explicitly since the unifier does not coerce 
;variable types

(define flatfun |∀x y.(atom(x)⊃flatfun(x)=(λY.X.Y))∧
                      (flatfun(X.Y)=(λZ.(flatfun(X))((flatfun(Y))(Z))))|
	(use high_order_definition
	     ue: ((atom_fun.|λx.λy.x.y|)
		  (bigfun.|λx y arb1 arb2.λz.arb1(arb2(z))|)) ))
 
(define flat |∀x y.flat(x,y)=(flatfun(x))(y)|)
 
;can verify sexp'ness as usual

(ue ((phi.|λx.∀z.sexp (flatfun(x))(z)|))  sexpinduction
    (open flatfun))
;∀X Z.SEXP (FLATFUN(X))(Z)
(label simpinfo)

;the fact about flat

(trw |∀x y z.(atom(x)⊃flat(x,y)=x.y)∧(flat(x.y,z)=flat(x,flat(y,z)))|
     (open flat flatfun))
;∀X Y Z.(ATOM X⊃FLAT(X,Y)=X.Y)∧FLAT(X.Y,Z)=FLAT(X,FLAT(Y,Z))